$\vdash$  $\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $p$:($a$:$A$ $\times$ $B$($a$)). ($p$.1) $\in$ $A$